open import Function using (_$_)
open import Algebra using ( Group )
open import Level using ( Level )
import Relation.Binary.EqReasoning as EqR
import  Algebra.Properties.Group

module Util where

-- Group util
module _ {c ℓ : Level} (g : Group c ℓ) where
  open Group g
  open EqR setoid
  open Algebra.Properties.Group g
  ε⁻¹≈ε : ε ⁻¹ ≈ ε
  ε⁻¹≈ε = begin
    ε ⁻¹ ≈⟨ sym $ identityʳ _ ⟩
    ε ⁻¹ ∙ ε ≈⟨ inverseˡ ε ⟩
    ε ∎
  
  ∙⁻¹-distribution : (x y : Carrier) → ((x ∙ y) ⁻¹) ≈ ((y ⁻¹) ∙ (x ⁻¹) )
  ∙⁻¹-distribution x y =   begin
    (x ∙ y) ⁻¹ ≈⟨ sym $ identityʳ _ ⟩
    (x ∙ y) ⁻¹ ∙ ε ≈⟨ ∙-cong refl (sym $ inverseʳ x) ⟩
    (x ∙ y) ⁻¹ ∙ (x ∙ x ⁻¹) ≈⟨ ∙-cong refl (∙-cong (sym $ identityʳ x) refl) ⟩
    (x ∙ y) ⁻¹ ∙ (x ∙ ε ∙ x ⁻¹) ≈⟨ ∙-cong refl (∙-cong (∙-cong refl (sym $ inverseʳ y)) refl) ⟩
    (x ∙ y) ⁻¹ ∙ (x ∙ (y ∙ y ⁻¹) ∙ x ⁻¹) ≈⟨ ∙-cong refl (∙-cong (sym $ assoc _ _ _) refl) ⟩
    (x ∙ y) ⁻¹ ∙ ((x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹) ≈⟨ ∙-cong refl (assoc _ _ _) ⟩
    (x ∙ y) ⁻¹ ∙ ((x ∙ y) ∙ (y ⁻¹ ∙ x ⁻¹)) ≈⟨ sym $ assoc _ _ _ ⟩
    (x ∙ y) ⁻¹ ∙ (x ∙ y) ∙ (y ⁻¹ ∙ x ⁻¹) ≈⟨ ∙-cong (inverseˡ _) refl ⟩
    ε ∙ (y ⁻¹ ∙ x ⁻¹) ≈⟨ identityˡ _ ⟩
    y ⁻¹ ∙ x ⁻¹ ∎
